open cic
open shared_names

pred SubElements[ffea: FullFledgedEA, elements: set EASE] {
	ffea.subElements.univ = elements
}

pred AllowedDeployment[ffea: FullFledgedEA, nodes: set ND] {
	ffea.node in nodes
}

pred AllowedEAsForSubElement[ffea: FullFledgedEA, allowedEAs: set EA] {
	ffea.ea in allowedEAs	
} 

pred AvailablePorts[ffea: FullFledgedEA, availablePorts: set EAP] {
	ffea.portSignatures.univ = availablePorts	
}

pred PortBinding[ffea1: FullFledgedEA, p1: EAP, ffea2: FullFledgedEA, p2: EAP] {
	ffea1.portSignatures[p1] = ffea2.portSignatures[p2]	
}

pred SignaturePropagation[ffea: FullFledgedEA, p1: EAP, p2: EAP] {
	ffea.portSignatures[p1] = ffea.portSignatures[p2]	
}

pred SupportedFeatures[ffea: FullFledgedEA, supportedFeatures: set FT] {
	ffea.features.univ in supportedFeatures
}

pred ProvidedFeatures[ffea: FullFledgedEA, f: set FT] {
	ffea.features.univ = f
}

pred DelegateFeatures[f: set FT, parent: FullFledgedEA, child: EASE] {
	all ft: f & parent.features.univ {
		parent.features[ft] = parent.subElements[child].features[ft]
	}
}

pred DelegateDeployment[from: FullFledgedEA, to: FullFledgedEA] {
	to.node = from.node
}

pred AvailableAttributes[ffea: FullFledgedEA, a: set AT] {
	ffea.attributes.univ in a
} 

pred AssignFeatureValue[ffea: FullFledgedEA, ft: FT, fv: FV] {
	ffea.features[ft] in fv 
}

pred AssignAttributeValue[ffea: FullFledgedEA, ft: FT, featureFieldName: FV->AV, at: AT] {
	ffea.features[ft].featureFieldName = ffea.attributes[at] 
}

-- Generated from the "FileLogger" partial element architecture
-- Image of the "FileLogger" EA
one sig EA_FileLogger extends EA {}
fact EA_FileLogger { 
  all ei: FullFledgedEA  | ei.ea = EA_FileLogger => {
	AllowedDeployment[ei, ND_A]		
	AvailablePorts[ei, EAPLP_CallIn + EAPLR_CallOut]
	no ei.subElements
			
	-- port signature delegation
	ei.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLR_CallOut]
	
	ProvidedFeatures[ei, FT_Logging]
	AvailableAttributes[ei, AT_FileName]
		
	AssignFeatureValue[ei, FT_Logging, FV_Logging_ToFile]
	AssignAttributeValue[ei, FT_Logging, fileName, AT_FileName]			
}}

-- Generated from the "RMIServerProxyWrapper" partial element architecture
-- Image of the "RMIServerProxyWrapper" EA specification
one sig EA_RMIServerProxyWrapper extends EA {}
fact EA_RMIServerProxyWrapper { all ei: FullFledgedEA  | ei.ea = EA_RMIServerProxyWrapper => {
	
	SubElements[ei, EASE_ServerProxy + EASE_SocketFactory]

	let ei_serverProxy = ei.subElements[EASE_ServerProxy] |
	let ei_socketFactory = ei.subElements[EASE_SocketFactory] {
	
		AllowedEAsForSubElement[ei_serverProxy, EA_RMIServerProxy]
		DelegateDeployment[ei, ei_serverProxy]
		AvailablePorts[ei_serverProxy, EAPLR_CallOut + EAPR_Line + EAPLR_SocketFactory]		

		AllowedEAsForSubElement[ei_socketFactory, EA_RMISocketFactory + EA_RMISSLHighSecuritySocketFactory]
		DelegateDeployment[ei, ei_socketFactory]		
		AvailablePorts[ei_socketFactory, EAPLP_Factory]

		PortBinding[ei_serverProxy, EAPLR_CallOut, ei, EAPLR_CallOut]
		PortBinding[ei_serverProxy, EAPR_Line, ei, EAPR_Line]
		PortBinding[ei_serverProxy, EAPLR_SocketFactory, ei_socketFactory, EAPLP_Factory]
	}

	no ei.portSignatures[EAPR_Line].entries.responsibleInstance & ei

	SupportedFeatures[ei, FT_Security]
	DelegateFeatures[FT_Security, ei, EASE_SocketFactory]
	
	no ei.attributes
}}

-- Generated from the "RPCServerUnit" partial element architecture
one sig EA_RPCServerUnit extends EA {}
fact EA_RPCServerUnit { all ei: FullFledgedEA  | ei.ea = EA_RPCServerUnit => {
	AllowedDeployment[ei, ND_A]

	SubElements[ei, EASE_ServerProxy]	

	let ei_serverProxy = ei.subElements[EASE_ServerProxy] {
		AllowedEAsForSubElement[ei_serverProxy, EA_RMIServerProxyWrapper]
		
		ei_serverProxy.node = ei.node
	
		AvailablePorts[ei_serverProxy, EAPLR_CallOut + EAPR_Line]
		
		PortBinding[ei_serverProxy, EAPR_Line, ei, EAPR_Line]
		PortBinding[ei_serverProxy, EAPLR_CallOut, ei, EAPLR_CallOut]		
	}

	no ei.portSignatures[EAPR_Line].entries.responsibleInstance & ei

	SupportedFeatures[ei, FT_Logging + FT_Security]
	DelegateFeatures[FT_Logging + FT_Security, ei, EASE_ServerProxy]
	
	no ei.attributes
}}


-- Generated from the "RPCClientUnit" partial element architecture
one sig EA_RPCClientUnit extends EA {}
fact EA_RPCClientUnit { all ei: FullFledgedEA  | ei.ea = EA_RPCClientUnit => {
	ei.node in ND_A

	ei.subElements.univ = EASE_ClientProxy

	let ei_clientProxy = ei.subElements[EASE_ClientProxy] {
		ei_clientProxy.ea in EA_RMIClientProxy
		ei_clientProxy.node = ei.node
	
		ei_clientProxy.portSignatures.univ = EAPLP_CallIn + EAPR_Line
		ei_clientProxy.portSignatures[EAPR_Line] = ei.portSignatures[EAPR_Line]
		ei_clientProxy.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLP_CallIn]
	}

	no ei.portSignatures[EAPR_Line].entries.responsibleInstance & ei

	all ft: ei.features.univ {
		ft in FT_Logging
		ft in FT_Logging => {
			ei.features[ft] = ei.subElements[EASE_ClientProxy].features[ft]
		}
	}

	no ei.attributes
}}


-- Generated from the "InterceptedRPCClientUnit" partial element architecture
one sig EA_InterceptedRPCClientUnit extends EA {}
fact EA_InterceptedRPCClientUnit { all ei: FullFledgedEA  | ei.ea = EA_InterceptedRPCClientUnit => {
	ei.node in ND_A

	ei.subElements.univ = EASE_ClientProxy + EASE_Interceptor

	let ei_clientProxy = ei.subElements[EASE_ClientProxy] |
	let ei_interceptor = ei.subElements[EASE_Interceptor] {
		ei_clientProxy.ea in EA_RMIClientProxy
		ei_clientProxy.node = ei.node

		ei_interceptor.ea in EA_ConsoleLogger + EA_FileLogger
		ei_interceptor.node = ei.node	

		ei_clientProxy.portSignatures.univ = EAPLP_CallIn + EAPR_Line
		ei_interceptor.portSignatures.univ = EAPLR_CallOut + EAPLP_CallIn
		ei_interceptor.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLP_CallIn]
		ei_interceptor.portSignatures[EAPLR_CallOut] = ei_clientProxy.portSignatures[EAPLP_CallIn]
		ei_clientProxy.portSignatures[EAPR_Line] = ei.portSignatures[EAPR_Line]
	}

	no ei.portSignatures[EAPR_Line].entries.responsibleInstance & ei

	all ft: ei.features.univ {
		ft in FT_Logging
		ft in FT_Logging => {
			ei.features[ft] = ei.subElements[EASE_ClientProxy].features[ft] ||
			ei.features[ft] = ei.subElements[EASE_Interceptor].features[ft]
		}
	}

	no ei.attributes
}}




-- Generated from the "RMIServerProxy" partial element architecture
one sig EA_RMIServerProxy extends EA {}
fact EA_RMIServerProxy { all ei: FullFledgedEA  | ei.ea = EA_RMIServerProxy => {
	ei.node in ND_A

	no ei.subElements

	some sbe_line: ei.portSignatures[EAPR_Line].entries {
		// rse_line is the only contribution of this instance to the signature
		ei.portSignatures[EAPR_Line].entries :> responsibleInstance.ei = sbe_line

		sbe_line.responsibleInstance = ei
		sbe_line.signature in S_RMIServer
		sbe_line.signature.javaSig = ei.portSignatures[EAPLR_CallOut]
	}
	
	ei.portSignatures[EAPLR_SocketFactory] = S_RMISocketFactoryItf

	no ei.features
	no ei.attributes
}}


-- Generated from the "RMISocketFactory" partial element architecture
one sig EA_RMISocketFactory extends EA {}
fact EA_RMISocketFactory { all ei: FullFledgedEA  | ei.ea = EA_RMISocketFactory => {
	ei.node in ND_A

	no ei.subElements

	ei.portSignatures[EAPLP_Factory] = S_RMISocketFactoryItf

	no ei.features
	no ei.attributes
}}


-- Generated from the "RMISSLHighSecuritySocketFactory" partial element architecture
one sig EA_RMISSLHighSecuritySocketFactory extends EA {}
fact EA_RMISSLHighSecuritySocketFactory { all ei: FullFledgedEA  | ei.ea = EA_RMISSLHighSecuritySocketFactory => {
	ei.node in ND_A

	no ei.subElements

	ei.portSignatures[EAPLP_Factory] = S_RMISocketFactoryItf

	ei.features.univ = FT_Security
	ei.features[FT_Security] = FV_Security_High

	no ei.attributes
}}


-- Generated from the "RMIClientProxy" partial element architecture
one sig EA_RMIClientProxy extends EA {}
fact EA_RMIClientProxy { all ei: FullFledgedEA  | ei.ea = EA_RMIClientProxy => {
	ei.node in ND_A

	no ei.subElements

	no ei.portSignatures[EAPR_Line].entries.responsibleInstance & ei
	some sbe_line: ei.portSignatures[EAPR_Line].entries {
		sbe_line.signature in S_RMIServer
		sbe_line.signature.javaSig = ei.portSignatures[EAPLP_CallIn]
	}

	no ei.features
	no ei.attributes
}}


-- Generated from the "ConsoleLogger" partial element architecture
one sig EA_ConsoleLogger extends EA {}
fact EA_ConsoleLogger { all ei: FullFledgedEA  | ei.ea = EA_ConsoleLogger => {
	ei.node in ND_A

	no ei.subElements

	ei.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLR_CallOut]

	ei.features.univ = FT_Logging
	ei.features[FT_Logging] = FV_Logging_ToConsole

	no ei.attributes
}}



